the_w:World, l:IdLnk, mss:(Msg List). onlnk(l;mss)  ({m:Msg| mlnk(m) = l}  List) 

latex

Definitions	t  T, x:A. B(x), t.1, onlnk(l;mss), mlnk(m), , Msg(M), Msg, P  Q, P & Q, P  Q
Lemmas	world wf, IdLnk wf, w-Msg wf, assert wf, eq lnk wf, filter type, subtype rel list, assert-eq-lnk